COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003	.hd206 FALL 1978
C00007 00004
C00008 00005	.cb |Proving|
C00021 ENDMK
C⊗;
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.place text;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.
.MACRO hw (DATE) ⊂
.   BEGIN TURNON "←"  NOFILL
←FINAL
←DATE
.   TURNOFF END ⊃
.
.itemmac
.
.PORTION MAINPORTION
.
.LSPFONT
.basicops 
.next page
.hd206 FALL 1978
.skip
.hw |December 14|
.cb |This test is open book and open note|

.cb |Programming|
.skip

	Write LISP programs for each of the functions described below.
The functions can be written in either internal or external notation.  Assume a
reasonable number of functions are system defined (e.g. APPEND, REVERSE, PLUS, etc.)
but when in doubt, write the function yourself.
.BEGIN INDENT 0,6

1)(16 pts.) Write a program ⊗variants[n] which yields a list of all the S-expressions in
NIL of size ⊗n. 
The following is a set of i/o pairs satisfying the function definition.

.BEGIN NOFILL
⊗⊗variant[$$0$] = ()⊗
⊗⊗variant[$$1$] = (NIL)⊗
⊗⊗variant[$$2$] = ((NIL. NIL))⊗
⊗⊗variant[$$3$] = ( (NIL .(NIL. NIL)) ((NIL . NIL) . NIL))⊗
.END

2) (16 pts.)The following is a program to compute the intersection of ⊗u and ⊗v where both
are lists of atoms.  Its running time in the worst case is ⊗length[u]*length[v]. 
Rewrite a version of ⊗intersection which runs in time ⊗length[u]+length[v].  Hint:
Use the property list of the atoms involved.

.begin  nofill select 2 

⊗⊗	intersection[u,v] ← ⊗
⊗⊗		qif qn u qthen qNIL⊗
⊗⊗		qelseif member[qa u,v] then [qa u] . intersection[qd u,v]⊗
⊗⊗		qelse intersection[qd u,v]⊗

.end

Why would this not work if ⊗u and ⊗v were not lists of atoms.

3) (16 pts.)Let ⊗x be a possibly re-entrant list structure.  Write the LISP function
⊗count[x] that gives the number of distinct vertices in x.  Hint: Use a variable
⊗u that lists vertices already seen.

4) (16 pts.)Write a program using RPLACA and RPLACD which yields a re-entrant list structure
corresponding to a graph in the notation described in the notes.  Thus
((A B C) (B A D) (C D E) (D B E)) becomes

.SKIP 10

Note that many of the atoms in the non-re-entrant list are representd by lists in
the re-entrant list.
You may use notations like ad x ← y instead of (RPLACA (CDR x) y).  This also
applies for RPLACD.

.END
.cb |Proving|
.skip

5)	(16 pts.)Given the following function descriptions prove the required theorem.
Be explicit and rigorous in recording your proof.  Justify each individual step
(i.e. function expansion, induction hypothesis, etc.).  The only theorems you may
assume have been previously proved are the associativity of append and that NIL
is the identity for append (on either side).
If you need a lemma, prove it.

.begin  nofill select 2 

⊗⊗	member[x,u] ← ⊗
⊗⊗		¬ qn u ∧ [x = [qa u] ∨ member[x, qd u]]⊗

⊗⊗	append[u,v] ← ⊗
⊗⊗		qif qn u qthen v⊗
⊗⊗		qelse [qa u] . append[qd u, v]⊗

.end

Prove: member[x,append[u,v]] ≡ member[x,u] ∨ member[x,v]

.skip 5
.cb |Programming & Proving|
.skip

6)	(20 pts.)
Write programs for the following two functions and prove the required
theorem.  You can use any lemmas proved in class.  Assume the list ⊗u is ordered
with no duplications.
.BEGIN INDENT 0,6

 ⊗insert[n,u] inserts the number ⊗n into the ordered list ⊗u and preserves the
 ordered and non-duplication properties of ⊗u. The
following is one i/o pair which satisfies the function definition.

⊗⊗⊗insert[$$(4 (1 2 5))$] = (1 2 4 5)⊗

⊗delete[n,u] deletes the number ⊗n from the ordered list ⊗u.  If ⊗n is not
 present then ⊗u remains unchanged.
The following is one i/o pair which satisfies the function definition.

⊗⊗⊗delete[$$(4 (1 2 4 5))$] = (1 2 5)⊗

Prove: ¬member[n,u] ⊃ [ delete[n,insert[n,u]] = u ]
.END